$\forall$${\it the\_es}$:ES, ${\it e'}$:E, $l$:IdLnk, $m$:Msg.
\\[0ex]($m$ $\in$ snds($l$;before(${\it e'}$))) $\Leftrightarrow$ ($\exists$$e$:E. ($e$ $<$loc ${\it e'}$) \& ($m$ $\in$ sends($l$;$e$)))